$\forall$$T$:Type, ${\it as}$:$T$ List, $i$:\{0$\ldots\,\parallel$${\it as}$$\parallel$\}, $j$:\{$i$$\ldots\,\parallel$${\it as}$$\parallel$\}. $\parallel$${\it as}$[$i$..$j$$^{-}$]$\parallel$ $=$ $j$$-$$i$